Sharpen and simplify the Section 8 all-deficit partition function - #49

Purpose

This stacked mathematics-and-exposition PR sits above #48. It isolates the finite product interface needed after the attained-demand support/deficit reindexing and rewrites the all-deficit part of Section VIII around one cellwise partition function.

It makes two independent improvements:

1. sum the complete positive-deficit fibre inside each selected cell before multiplying cells, removing the artificial factor counting admissible deficits;
2. use the stronger three-quarter binary-exponent budget implied by 2h<m.

The old generic cardinality endpoint gave

O(n^(2/3) (log n)^(7/3)).

Geometric summation alone gives

O(n^(2/3) (log n)^(4/3)).

The three-quarter budget improves the direct one-line estimate further to

O(sqrt(n) (log n)^(3/2)).

An optional first-term/tail decomposition gives

O((log n)^4),

but the proposed manuscript insert retains the shorter one-line geometric proof.

Finite Lean interfaces

Cellwise partition function

625/formalization/Erdos625/Section8SharpDeficitProduct.lean proves:

sum_nearSkeletonChoiceWeight_le_product_of_local_sums
sum_nearSkeletonChoiceWeight_le_uniform_local_sum
sum_nearSkeletonChoiceWeight_le_cellwise_two_rho
sum_nearSkeletonChoiceWeight_le_uniform_two_rho

The strongest form retains a separate local bound sigma_c in every selected cell:

sum_global_choices weight(choice)
  <= product_c (1 + sigma_c),

provided the complete positive-deficit fibre in cell c is at most sigma_c.

Thus the sixteen endpoint-type charges need not be replaced by one maximum until the final optional uniformization. The module also proves that the local charge 2*rho is no worse than the earlier U*rho cardinality charge for U >= 2.

Three-quarter exponent budget

625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean proves

h * floor((3m-1)/4)
  <= h*m - h*(h+1)/2

whenever 2h<m. The coefficient differs from the optimal integer coefficient floor(3m/4) by at most one and has the same phase asymptotics. It improves the common local base from

n*m / 2^floor(2m/3)

to

n*m / 2^floor((3m-1)/4).

Mathematical application

For endpoint sizes m,m+d and deficit h, the exact aggregate local ratio is

R_{m,d}(h)
  = C(m,h)/((d+1)...(d+h)) * 2^(-hm+h(h+1)/2).

The high condition and the new arithmetic theorem give

n^h R_{m,d}(h) <= rho(m)^h,

rho(m) = n*m / 2^floor((3m-1)/4).

When rho(m) <= 1/2, the whole positive-deficit fibre satisfies

sum_{h>=1} n^h R_{m,d}(h)
  <= rho(m)/(1-rho(m))
  <= 2*rho(m).

Therefore, for fixed support P,

sum_h w(P,m-h)
  <= w_full(P) * product_{e in P} (1 + 2*rho_e).

At the four-size phase,

rho_n = O((log n)^(5/2)/sqrt(n)),
|P| <= k_co = Theta(n/log n),

so the direct all-deficit exponent is

O(sqrt(n) (log n)^(3/2)).

Together with endpoint transportation,

O(sqrt(n) (log n)^(3/2)) + O(sqrt(n log n))
  = o(n/(log n)^4).

For the optional head--tail refinement,

n R_{m,d}(1) = O((log n)^3/n),

sum_{h>=2} n^h R_{m,d}(h)
  <= rho_n^2/(1-rho_n)
  = O((log n)^5/n),

which yields total all-deficit exponent O((log n)^4) over at most O(n/log n) selected cells.

Readability rewrite

The PR adds:

625/proofs/SECTION8_SHARP_DEFICIT_PRODUCT_AND_REWRITE.md
625/arxiv/SECTION8_SHARP_DEFICIT_INSERT_V2.tex

The proof is organized into four auditable steps:

1. exact attained-demand reindexing;
2. one-cell aggregate ratio and one global denominator loss;
3. cellwise geometric summation before summing supports;
4. full-endpoint transportation.

The note includes a two-cell example showing why there is one global (n)_J normalization and no extra ordering factor.

The TeX fragment is deliberately not included by main.tex. It has an explicit audit boundary and may be integrated only after the reindexing and pointwise aggregate-weight identities are green.

Exact Python checks

The optimized standard-library script

625/experiments/section8_sharp_deficit_product.py

checks under ordinary and optimized Python:

• the exact aggregate local ratio;
• both the two-thirds and three-quarter exponent budgets;
• charged local ratios for many finite values;
• finite geometric sums and the 2*rho bound;
• the optional first-term plus geometric-tail bound;
• exact partition-function factorization over distinguishable cells;
• the 2*rho versus U*rho comparison;
• retention of cellwise endpoint-type charges;
• all error scales relative to n/(log n)^4.

These checks are finite arithmetic and diagnostics, not a replacement for the remaining Lean reindexing or phase asymptotics.

Files

• 625/formalization/Erdos625/Section8SharpDeficitProduct.lean
• 625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean
• 625/proofs/SECTION8_SHARP_DEFICIT_PRODUCT_AND_REWRITE.md
• 625/arxiv/SECTION8_SHARP_DEFICIT_INSERT_V2.tex
• 625/experiments/section8_sharp_deficit_product.py
• .github/workflows/erdos625-sharp-deficit-product.yml

Validation

On head 8f3f5028111d6a68f3373344cb0bf3dae77fbafc, the dedicated workflow passed all focused gates:

• placeholder/project-axiom rejection;
• Lean 4.31 warning-fatal builds of both new formal modules;
• exact checker under ordinary Python;
• exact checker under python -O;
• reader-facing TeX marker, equation-label, and brace checks.

The repository-wide Lean workflow is separate and was still running when this status was recorded.

Scope boundary

This PR does not yet prove:

• that the Reindex attained high demands by block support and bounded deficits #48 encoding is green on the integrated branch;
• the pointwise equality between profileHighSkeletonWeight and the aggregate partial-cell weight;
• the specialization of the local geometric estimate to every attained midpoint cell;
• the final bare-skeleton estimate;
• Proposition 9.2;
• Erdos625Statement.

It sharpens and simplifies the exact product interface that will be used once those finite identifications are connected. Keep the PR draft until the stacked reindexing and weight-identification seams are closed.